Nuprl Lemma : w-TA_wf
11,40
postcript
pdf
w
:World.
w
.TA
Id
Id
Type
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
w
.TA
,
t
.1
,
t
.2
,
World
Lemmas
world
wf
origin
w:World. w.TA 
Id
IdType w:World. w.TA IdIdType x:A. B(x) T